Section: New Results

Decision procedures

A certificate framework for DPLL(T)

Participants : Min Zhou, Fei He, Bow-Yaw Wang, Wenrui Meng.

Satisfiability Modulo Theories (SMT) techniques are widely used nowadays. SMT solvers are used to decide the satisfiability of first-order formulas. When an SMT solver is invoked, it is important to ensure correctness of the result. For this purpose, we proposed a certificate framework based on DPLL(T), including generation of certificates and verification of certificates. Some properties are discussed and proved theoretically. The certificate is easy to generate because it only needs minor modification to the existing SMT solvers. Experiment results show that the overhead for certificates generation is only 10%. Moreover, verifying the certificate requires few memory and time, which outperforms other approaches.

Automated verification of termination certificates

Participants : Frédéric Blanqui, Kim-Quyen Ly, Sidi Ould Biha.

The research community on rewriting developed a grammar for termination certificates called CPF [29] (given by a XML Schema file). Our goal is to develop a safe, modular and efficient termination certificate verifier based on the formal library of mathematical results on termination called CoLoR that has been developed for the proof assistant Coq [11] .

Because the CPF format is regularly modified and extended with new features, it is useful to have a tool that can automatically generate data structures, parsers and pretty-printers for that format. Hence, we developed a first version of such a tool in OCaml.

Once we got a representation of termination certificates in Coq, we could start defining a boolean function checking the correctness of a certificate, and formally prove its correctness. For the moment, we only considered the case of polynomial interpretations on integers. The proof is almost finished. To do so, we had to modify some of the CoLoR files to be able to use its results (transformation of modules into records that are first-class objects). The use of dependent types in CoLoR makes also definitions and proofs much more difficult.

Proving computational geometry algorithms in TLA+2

Participants : Hui Kong, Hehua Zhang, Ming Gu.

Geometric algorithms are widely used in many scientific fields like computer vision, computer graphics. To guarantee the correctness of these algorithms, it is important to apply formal method to them. In this work, we propose an approach to proving the correctness of geometric algorithms [22] . The main contribution is that a set of proof decomposition rules is proposed which can help improve the automation of the proof of geometric algorithms. We choose TLA+2, a structural specification and proof language, as our experiment environment. The case study on a classical convex hull algorithm shows the usability of the method.